perm filename HOMOMO.NOT[257,JMC] blob sn#136991 filedate 1974-12-19 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	The homomorphism theorem.
C00003 ENDMK
C⊗;
The homomorphism theorem.

(∀f1 f2. g..f1 = f2..h ⊃ g..F1(f1)) = F2(f2)..h) ⊃ g..Y(F1) = Y(F2)..h

Here .. denotes composition of functions.

A second and easier theorem

(∀f. g..F1(f) = F2(g..f)) ⊃ g..Y(F1) = Y(F2)